COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	the new rewriter in ekl seems to work: here is an example of its power:
C00004 ENDMK
C⊗;
;the new rewriter in ekl seems to work: here is an example of its power:
;a one line proof of associativity of append

(get-proofs lispax)
(proof append)
(DECL NEWAPPEND (TYPE: |(GROUND⊗(GROUND*))→GROUND|) (SYNTYPE: CONSTANT)
  (INFIXNAME: **) (BINDINGPOWER: 840))

(AXIOM |∀U V.U**V=(IF NULL U THEN V ELSE CAR U.(CDR U**V))|)
(label appendef)

(AXIOM |∀U V.LISTP U**V|) (label simpinfo) (label sortinfo)

;you can now deduce associativity as follows:
(ue (phi |λu.(u**v)**w=u**(v**w)|) listinduction (use appendef) sortinfo simpinfo)
∀U.(U ** V) ** W=U ** (V ** W)

;or:
(ue (phi |λu.(u**v)**w=u**(v**w)|) listinduction nil appendef sortinfo simpinfo)
∀U.(U ** V) ** W=U ** (V ** W)